Nuprl Definition : kind 11,40

kind(e) == case info(e) of inl(p) => locl(p.2) | inr(q) => rcv(q.1.1,q.2) 
latex



clarification:

kind(info;e) == case info(e) of inl(p) => locl(p.2) | inr(q) => rcv(q.1.1,q.2) 
latex


Definitionscase b of inl(x) => s(x) | inr(y) => t(y), f(a), locl(a), rcv(l,tg), t.1, t.2
FDL editor aliaseskind

origin